High integrity software is software that must be trusted to work dependably in some critical function, and whose failure to do so may have catastrophic results, such as serious injury, loss of life or property, business failure or breach of security. Some examples include software used in safety systems of nuclear power plants, medical devices, electronic banking, air traffic control, automated manufacturing, and military systems. The importance of high quality, low defect software is apparent in such critical situations. However, high integrity software is also important in more mundane business areas where defective software is often the norm.
Formal verification is the process of checking whether a design satisfies some requirements or properties. In order to formally verify a design, it must first be converted into a more condensed, verifiable format. The design is specified as a set of interacting systems, each having a finite number of configurations or states. States and transition between states constitute finite state machines (FSMs). The entire system is a FSM that can be obtained by composing the FSMs associated with each component. The first step in verification consists of obtaining a complete FSM description of the system. Given a present state (or current configuration), the next state (or successive configuration) of a FSM can be written as a function of its present state and inputs (transition function or transition relation). Formal verification attempts to execute every possible computational path with every possible state value to prove every possible state is consistent.
A software program executing on a computer typically uses three types of memory: program memory, stack memory and heap memory. Program instructions are typically stored in program memory. Parameters, return values and variables local to procedures are typically stored in stack memory. Heap memory is typically used for dynamic memory requests made during program execution. Heap memory typically comprises a portion of the computer's random access memory (RAM). Whether static or dynamic memory allocation is used in the compiled code depends on the programming construct used by the programmer.
Turning now to FIG. 1, a flow diagram that illustrates a typical method for writing, compiling and executing a software program that dynamically allocates memory during program execution is presented. At 100, a software program that includes dynamic memory allocation is written. At 105, the software program is compiled. At 110, the software program is executed, dynamically allocating memory at run-time.
Unfortunately, dynamic allocation of memory during runtime is relatively inefficient. Runtime allocation of memory typically requires a relatively large number of processor cycles. Also, each access of the dynamically allocated memory typically requires more processor cycles than accessing a statically allocated variable because loading a dynamically allocated variable includes resolving indirect memory references. Loading a dynamically allocated variable requires loading a pointer value that contains the address of the dynamically allocated variable and then using the pointer value as an address to load the variable data.
Program verification is also complicated by dynamic memory allocation due to the many factors that can affect the size of a dynamic memory allocation. Dynamic memory allocation makes the state of a module dependent upon a runtime component that performs memory allocation. Coupling the state of the memory allocation to the state of the module that uses it complicates the state engine that is verified. This problem is especially acute for developers of programs targeted to devices having relatively tight memory constraints.
A programmer may perform static allocation of memory by hand. However, this process is particularly error-prone, typically resulting in low quality, low integrity software.
Accordingly, what is needed is a solution that increases program verifiability. A further need exists for such a solution that reduces dynamic memory allocation. Yet a further need exists for such a solution that simplifies memory management. Yet a further need exists for such a solution that automates memory management for programs targeted to devices having relatively limited memory.